rationals $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$quotient(b{-}union($\mathbb{Z}$; (:$\mathbb{Z}$ $\times$ int\_nzero)); $r$,$s$.(qeq($r$; $s$) = tt $\in$ $\mathbb{B}$))